a, b:Id. Dec(a = b) 

latex

Definitions	Id, t  T, x:A. B(x), a = b, b, Dec(P), Prop, P  Q, P  Q, P & Q, P  Q, x. t(x)
Lemmas	all functionality wrt iff, decidable functionality, assert-eq-id, decidable wf, assert wf, decidable assert, eq id wf, Id wf